T:Type, A:(T). (f:detach_fun(T;A). True)  (x:T. Dec((A(x)))) 

latex

Up	gen algebra 1
Definitions of Statement	detach_fun(T;A)
Definitions	t  T, P  Q, P  Q, P & Q, detach_fun(T;A), x:A. B(x), P  Q, , x:A. B(x), x. t(x), True, T, P  Q, Dec(P), A, if b then t else f fi , ff, tt, b, x(s), SqStable(P), Unit, , False,
Lemmas	decidable wf, true wf, assert wf, squash wf, iff wf, bool wf, sq stable squash, decidable assert, sq stable from decidable, sq stable implies, rev implies wf, sq stable and, sq stable all, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bfalse wf, btrue wf, false wf